\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\Rightarrow$ \=(connex(\{$e$:E$\mid$ $P$($e$)\} ;$R$$^{\mbox{\scriptsize $\ast$}}$)\+
\\[0ex]c$\wedge$ ($R$\^{}+$\mid$$P$ $\Lleftarrow\!\Rrightarrow$\{E\} $x$,$y$:E. ($x$ $<$ $y$)$\mid$$P$)
\\[0ex]c$\wedge$ ($R$$\mid$$P$\^{}+ $\Lleftarrow\!\Rrightarrow$\{E\} $R$\^{}+$\mid$$P$)
\\[0ex]c$\wedge$ ($R$$\mid$$P$ $\Lleftarrow\!\Rrightarrow$\{E\} $R$$\mid$$P$\^{}+!)
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$$\mid$$P$\^{}+($x$,$y$)) $\Rightarrow$ ($R$$\mid$$P$(${\it y'}$,$y$)) $\Rightarrow$ (($R$$\mid$$P$$^{\mbox{\scriptsize $\ast$}}$)($x$,${\it y'}$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$$\mid$$P$\^{}+($x$,$y$)) $\Rightarrow$ ($R$$\mid$$P$(${\it x'}$,$x$)) $\Rightarrow$ ($R$$\mid$$P$(${\it y'}$,$y$)) $\Rightarrow$ ($R$$\mid$$P$\^{}+(${\it x'}$,${\it y'}$))))
\-
\end{tabbing}